Inference at * 
Iof proof for Lemma can-apply-p-restrict:


  A, B:Type, f:(A(B + Top)), P:(A), p:(x:A. Dec(P(x))), x:A.
  (can-apply(p-restrict(f;p);x))  ((can-apply(f;x)) & P(x)) 

latex

 by ((((UnivCD ) 
CollapseTHENA (Auto))) 
CollapseTHEN (((Unfold `p-restrict` 0) 
CollapseTHEN (
Co((((RWO "can-apply-compose-iff" 0) 
THEN (MaAuto))) 
CollapseTHEN (((((
CoAll (RWO "do-apply-p-filter")) 
CollapseTHEN (Auto))) 
CollapseTHEN (((
CoAll (RWO "can-apply-p-filter")) 
CollapseTHEN (Auto)))))))))) 

latex

Co.

Definitions	p-restrict(f;p), s = t, False, inl x , inr x , A c B, case b of inl(x) => s(x) | inr(y) => t(y), tt, ff, Unit, if b then t else f fi , Dec(P), A, P  Q, P & Q, x:A  B(x), b, , can-apply(f;x), do-apply(f;x), p-filter(f), left + right, Top, T, f(a), x. t(x), P  Q, P  Q, x:AB(x), True, t  T, x(s), x:A. B(x), , Type
Lemmas	iff functionality wrt iff, can-apply-compose-iff, do-apply wf, btrue wf, bfalse wf, can-apply-p-filter, assert wf, can-apply wf, do-apply-p-filter